\begin{tabbing}
$\forall$${\it es}$:event\_system\{i:l\}, $x$,$i$:Id, $T$:Type, $c$:$T$.
\\[0ex]($\forall$$x$,$y$:$T$. decidable(($x$ = $y$ $\in$ $T$)))
\\[0ex]$\Rightarrow$ es{-}dtype(${\it es}$; $i$; $x$; $T$)
\\[0ex]$\Rightarrow$ ($\forall$$e$:es{-}E(${\it es}$). (loc($e$) = $i$) $\Rightarrow$ ($\uparrow$es{-}first(${\it es}$; $e$)) $\Rightarrow$ (es{-}when(${\it es}$; $x$; $e$) = $c$))
\\[0ex]$\Rightarrow$ \=($\forall$${\it e'}$:es{-}E(${\it es}$). \+
\\[0ex](loc(${\it e'}$) = $i$)
\\[0ex]$\Rightarrow$ ($\neg$(es{-}after(${\it es}$; $x$; ${\it e'}$) = $c$))
\\[0ex]$\Rightarrow$ ($\exists$\=${\it ev}$:es{-}E(${\it es}$)\+
\\[0ex](es{-}le(${\it es}$; ${\it ev}$; ${\it e'}$) $\wedge$ ($\neg$(es{-}after(${\it es}$; $x$; ${\it ev}$) = es{-}when(${\it es}$; $x$; ${\it ev}$) $\in$ $T$)))))
\-\-
\end{tabbing}